# 1. parenthesize every sentence into unary function applications, either leftward or rightward
# 2. the type of a sentence in boolean
# 3. thing42:chair, thing23:chair
#    chair is predicate that is true of things that are chairs and false of things that are not
#    chairs
#    the type of a noun is thing->boolean
# 4. A N --> A(N)
#    D N --> D(N)
#    N PP ---> PP(N)
#    NP VP --> VP(NP)
#    P NP --> P(NP)
# 5. Every word is going to be modeled as a lambda expression.

primitive type boolean
primitive type thing
typedef N = thing->boolean = thing->S
typedef A = N->N = (thing->S)->(thing->S) = (thing->boolean)->(thing->boolean)
typedef D = N->NP
typedef P = NP->PP = NP->(N<-N) = NP->((thing->S)<-(thing->S))
          = NP->((thing->boolean)<-(thing->boolean))
typedef Vintrans = VP = S<-NP = boolean<-NP
typedef Vtrans = NP->VP = NP->(S<-NP) = NP->(boolean<-NP)
typedef NP =
typedef VP = S<-NP = boolean<-NP
typedef S = boolean
typedef PP = N<-N = (thing->S)<-(thing->S) = (thing->boolean)<-(thing->boolean)

every = (
    lambda noun: (
        lambda noun1: (
            every(lambda x: noun(x)->noun1(x)))))

some = (
    lambda noun: (
        lambda noun1: (
            some(lambda x: noun(x) and noun1(x)))))

pawn = (lambda x: pawn(x))

square = (lambda x: square(x))

is_on1 = (
    lambda object_np: (
        lambda subject_np: (
            subject_np(lambda x: object_np(lambda y: on(x, y))))))

is_on2 = (
    lambda object_np: (
        lambda subject_np: (
            object_np(lambda y: subject_np(lambda x: on(x, y))))))

# Every pawn is on some square

# Every pawn is_on some square

((Every pawn) (is_on (some square)))

is_on(every(pawn))(some(square))

is_on1(every(pawn))(some(square))
is_on2(every(pawn))(some(square))

every(pawn)= ((
    lambda noun: (
        lambda noun1: (
            every(lambda x: noun(x)->noun1(x)))))
              ((lambda x: pawn(x))))

# eta reduction

every(pawn)= ((
    lambda noun: (
        lambda noun1: (
            every(lambda x: noun(x)->noun1(x)))))
              (pawn))

# beta reduction redex

every(pawn)= (
    lambda noun1: (
        every(lambda x: pawn(x)->noun1(x))))

some(square) = (
    (
        lambda noun: (
            lambda noun1: (
                some(lambda x: noun(x) and noun1(x)))))
    ((lambda x: square(x))))

# eta reduction

some(square) = (
    (
        lambda noun: (
            lambda noun1: (
                some(lambda x: noun(x) and noun1(x)))))
    (square))

# beta reduction

some(square) = (
    lambda noun1: (
        some(lambda x: square(x) and noun1(x))))

every(pawn)= (
    lambda noun1: (
        every(lambda x: pawn(x)->noun1(x))))

some(square) = (
    lambda noun1: (
        some(lambda x: square(x) and noun1(x))))

is_on1 = (
    lambda object_np: (
        lambda subject_np: (
            subject_np(lambda x: object_np(lambda y: on(x, y))))))
is_on1(every(pawn))(some(square)) = (is_on1(
    lambda noun1: (
        every(lambda x: pawn(x)->noun1(x))))
                                     (
                                         lambda noun1: (
                                             some(lambda x: square(x) and noun1(x)))))


(
    lambda object_np: (
        lambda subject_np: (
            subject_np(lambda x: object_np(lambda y: on(x, y))))))
(
    lambda noun1: (
        every(lambda x: pawn(x)->noun1(x))))

(
    lambda subject_np: (
        subject_np(lambda x: (
            lambda noun1: (
                every(lambda x: pawn(x)->noun1(x))))
                   (lambda y: on(x, y)))))

(
    lambda subject_np: (
        subject_np(lambda x: (
            lambda noun1: (
                every(lambda x: pawn(x)->noun1(x))))
                   (lambda y: on(x, y)))))
(
    lambda noun1: (
        some(lambda x: square(x) and noun1(x))))

(
    lambda noun1: (
        some(lambda x: square(x) and noun1(x))))
(lambda x: (
            lambda noun1: (
                every(lambda x: pawn(x)->noun1(x))))
                   (lambda y: on(x, y)))